The one-page cheat sheet.html (3692B)
1 <html> 2 <head> 3 <link rel="Stylesheet" type="text/css" href="style.css" /> 4 <title>The one-page cheat sheet</title> 5 <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> 6 </head> 7 <body> 8 <a href="index.html">Index</a> 9 <hr> 10 <div class="content"> 11 12 <div id="One-page cheat sheet"><h2 id="One-page cheat sheet" class="header"><a href="#One-page cheat sheet">One-page cheat sheet</a></h2></div> 13 <div id="One-page cheat sheet-Definitions"><h3 id="Definitions" class="header"><a href="#One-page cheat sheet-Definitions">Definitions</a></h3></div> 14 <ul> 15 <li> 16 Model is: 17 18 <ul> 19 <li> 20 set A - domain 21 22 <li> 23 interpretation operation for predicate and function symbols 24 25 </ul> 26 <li> 27 satisfiable: some model & environment where it's true 28 29 <li> 30 valid: true in all models and environments 31 32 <li> 33 derivable: can be proven without global hypothesis 34 35 <li> 36 tautology: true under any truth assignment (valid) 37 38 <li> 39 soundness: ⊢ A → ⊨ A (from syntax to semantics) 40 41 <li> 42 completeness: ⊨ A → ⊢ A (from semantics to syntax) 43 44 <li> 45 partial order: antisymmetric, reflexive, transitive 46 47 <ul> 48 <li> 49 memo technique -- p*<span id="One-page cheat sheet-Definitions-art"></span><strong id="art">art</strong>*ial means *<span id="One-page cheat sheet-Definitions-a"></span><strong id="a">a</strong>*ntisymmetric, *<span id="One-page cheat sheet-Definitions-r"></span><strong id="r">r</strong>*eflexive, *<span id="One-page cheat sheet-Definitions-t"></span><strong id="t">t</strong>*ransitive 50 51 <li> 52 strict means irreflexive 53 54 </ul> 55 <li> 56 total order: partial order & ∀ ab: R(a,b) ∨ R(b,a) 57 58 <ul> 59 <li> 60 strict: ∀ ab: R(a,b) ∨ a = b ∨ R(b,a) 61 62 </ul> 63 <li> 64 equivalence relation: has all three properties in the positive (symmetric, reflexive, transitive) 65 66 </ul> 67 68 <p> 69 environment is used to interpret free variables 70 </p> 71 <div id="One-page cheat sheet-Modal logic"><h3 id="Modal logic" class="header"><a href="#One-page cheat sheet-Modal logic">Modal logic</a></h3></div> 72 <ul> 73 <li> 74 □ Φ: true in world if true in all related worlds (if no related, true). 75 76 <li> 77 ◇ Φ: true in world if true in some related world (if no related, false). 78 79 </ul> 80 81 <p> 82 M,w ⊩ Φ: Φ true in world w of Kripke model M (true in model if true in every world) 83 </p> 84 85 <p> 86 Φ valid in frame if true with every labelling. 87 </p> 88 89 <p> 90 frame = Kripke - labels 91 </p> 92 93 <div id="One-page cheat sheet-Metatheorems"><h3 id="Metatheorems" class="header"><a href="#One-page cheat sheet-Metatheorems">Metatheorems</a></h3></div> 94 <ul> 95 <li> 96 consistent: has a model 97 98 <li> 99 syntactically consistent: can't derive ⊥ 100 101 <li> 102 compactness: if Γ is consistent, every finite subset of Γ is also consistent 103 104 </ul> 105 106 <div id="One-page cheat sheet-Definability"><h3 id="Definability" class="header"><a href="#One-page cheat sheet-Definability">Definability</a></h3></div> 107 <p> 108 Model finiteness is undefinable. 109 </p> 110 111 <p> 112 Model infiniteness is definable by a set of formulas. 113 </p> 114 115 <p> 116 In predicate logic, only unreachability by n steps is definable, and only by a set of sentences. 117 </p> 118 119 <div id="One-page cheat sheet-Decidability"><h3 id="Decidability" class="header"><a href="#One-page cheat sheet-Decidability">Decidability</a></h3></div> 120 <p> 121 Y ⊆ I decidable if program can tell for every i ∈ I whether i ∈ Y. I set, Y predicate on set. 122 </p> 123 124 <p> 125 Undecidable: termination, PCP, validity, provability, satisfiability. 126 </p> 127 128 <p> 129 Termination can be reduced to PCP, which can be reduced to validity. 130 </p> 131 132 <p> 133 Incompleteness theorems: every non-trivial formal system is 134 </p> 135 <ul> 136 <li> 137 either incomplete (valid but not derivable) 138 139 <li> 140 or inconsistent (doesn't have a model, or entails ⊥) 141 142 </ul> 143 144 </div> 145 </body> 146 </html>